Introduction to TLA+

Abhijit Paul

<2024-08-26 সোম>

TLA+ niche

  1. In TLA, every variable is a set
  2. In B′ = A + 3 ∧ A′ = 4 ⇔ A′ = 4 ∧ B′ = A + 3. This is unlike programming languages. Its because TLA is not programming language. Its Math and in math, X ∧ YY = Y ∧ X.
  3. In TLA, array is mathematical function, index set is domain and values are range. So its defined like. e.g. sqr = [i ∈ 1..42 → i2]. So sqr[3] = 9.

Non-deterministic C Code

Let us write our first program after installing TLA+ toolbox and opening the toolbox. We try to write the following C code segment in TLA+.

void main(){
  int x;
  x = someNumber();
  x = x+1;
}

To write it into TLA+,

And the ASCII version for it is:

------------------------------- MODULE first -------------------------------
EXTENDS integers
VARIABLE x, pc

init == (x=0) /\ (pc = "start")

next == \/ /\ pc = "start"
           /\ x' \in 1..1000
           /\ pc' = "middle"
        \/ /\ pc = "middle"
           /\ x' = x + 1
           /\ pc' = "exit" 


=============================================================================
\* Modification History
\* Last modified Mon Aug 26 20:42:38 BDT 2024 by abhijit
\* Created Mon Aug 26 20:15:57 BDT 2024 by abhijit

Die Hard

It is interesting how many different solution the invariants bigjar /= 4 can come up with!

------------------------------ MODULE diehard ------------------------------
EXTENDS Integers
VARIABLES bigjar, smalljar

TypeOK == bigjar \in 0..5 /\ smalljar \in 0..3

Init == bigjar = 0 /\ smalljar = 0

BigToSmall == IF bigjar + smalljar <= 3
                THEN 
                    /\ smalljar' = bigjar + smalljar 
                    /\ bigjar' = 0
              ELSE 
                    /\ bigjar' = bigjar - (3-smalljar) 
                    /\ smalljar' = 3

SmallToBig == IF bigjar + smalljar <= 5
                THEN 
                /\ bigjar' = bigjar + smalljar 
                /\ smalljar' = 0
              ELSE 
               /\ smalljar' = smalljar - (5-bigjar) 
               /\ bigjar' = 5

EmptySmall == smalljar' = 0 /\ bigjar' = bigjar
EmptyBig == bigjar' = 0 /\ smalljar' = smalljar 
FillSmall == smalljar' = 3 /\ bigjar' = bigjar
FillBig == bigjar' = 5 /\ smalljar' = smalljar

Next == BigToSmall \/ SmallToBig \/ EmptySmall \/ EmptyBig \/ FillSmall \/ FillBig
=============================================================================

Transaction Commit

A marriage or love consists of the followings steps (Hey, i won't know about it. This is what the books says >:3

  1. Unprepared stage
  2. Prepared stage
  3. Committed or aborted stage (hmm cheating perhaps)

This wedding can be compared to a database transaction. A transactions can commit if all resource managers (RM) are prepared to commit and is aborted otherwise. However, the unsure state is usually called working state of RM.

Now let us write a spec for it.

  1. In TLA+, every value is a set. Even 42 and "abc" are sets. But TLA+ does not know what their elements are. So it can't evaluate 42 "abc" as True or False.

  2. rmState is an array indexed by RMs. So rmState[r] is the state of RM r.

  3. In TLA+, arrays are functions. So array is defined as [domain -> range]. e.g. [rmState ∈ {"working", "prepared", "committed", "aborted"}].

  4. Some harder definitions of functions/array can be: rmState = [r ∈ RM → "working"]. Note that we use |-> symbol since we are assigning value.

  5. Similar to above [variable ∈ set → expression] notation, we can write [i ∈ 1..42 → i2]

  6. canCommit: One can commit if all RMs are already committed or prepared to commit.

  7. notCommitted: RM r can abort only when no other RM is committed.

    The final code is:

Paxos Commit

What happens if RM fails?

Resources

100 TLA+ exercise